(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4.
The certificate found is represented by the following graph.
Start state: 1067
Accept states: [1068, 1069, 1070, 1071, 1072, 1073]
Transitions:
1067→1068[p_1|0]
1067→1069[f_1|0]
1067→1070[g_1|0]
1067→1071[j_1|0]
1067→1072[half_1|0]
1067→1073[rd_1|0]
1067→1067[0_1|0, s_1|0]
1067→1074[p_1|1]
1067→1077[s_1|1]
1067→1084[rd_1|1]
1067→1092[s_1|1]
1067→1097[s_1|1]
1067→1107[s_1|1]
1067→1117[s_1|1]
1067→1075[s_1|1]
1067→1079[s_1|2]
1067→1099[s_1|2]
1067→1109[p_1|2]
1067→1110[s_1|1]
1067→1112[f_1|1, f_1|2]
1067→1081[half_1|2]
1067→1132[s_1|2]
1067→1101[s_1|2]
1067→1121[half_1|2]
1067→1122[s_1|2]
1067→1124[p_1|2, p_1|3]
1067→1134[s_1|3]
1067→1125[s_1|1]
1067→1127[f_1|1, f_1|2]
1067→1136[s_1|3]
1067→1142[s_1|3]
1067→1144[p_1|3, p_1|4]
1067→1145[s_1|1]
1067→1147[f_1|1, f_1|2]
1074→1075[s_1|1]
1075→1076[s_1|1]
1076→1068[0_1|1]
1076→1074[0_1|1]
1076→1109[0_1|1]
1076→1124[0_1|1]
1076→1144[0_1|1]
1077→1078[p_1|1]
1078→1079[s_1|1]
1078→1081[half_1|2]
1079→1080[p_1|1]
1080→1081[half_1|1]
1081→1082[s_1|1]
1082→1083[s_1|1]
1083→1072[0_1|1]
1083→1081[0_1|1]
1083→1121[0_1|1]
1084→1085[0_1|1]
1085→1086[s_1|1]
1086→1087[0_1|1]
1087→1088[0_1|1]
1088→1089[0_1|1]
1089→1090[0_1|1]
1090→1091[s_1|1]
1091→1073[0_1|1]
1091→1084[0_1|1]
1092→1093[s_1|1]
1092→1095[g_1|2]
1093→1094[p_1|1]
1094→1095[g_1|1]
1095→1096[s_1|1]
1095→1113[s_1|2]
1095→1115[s_1|2]
1095→1128[s_1|2]
1095→1130[s_1|2, s_1|3]
1095→1148[s_1|2]
1095→1150[s_1|2, s_1|3]
1096→1069[p_1|1]
1096→1112[p_1|1]
1096→1127[p_1|1]
1096→1147[p_1|1]
1097→1098[p_1|1]
1098→1099[s_1|1]
1098→1101[s_1|2]
1098→1122[s_1|2]
1098→1124[p_1|2, p_1|3]
1099→1100[p_1|1]
1100→1101[s_1|1]
1100→1122[s_1|2]
1100→1124[p_1|3]
1101→1102[j_1|1]
1102→1103[s_1|1]
1103→1104[s_1|1]
1104→1105[s_1|1]
1104→1070[p_1|2]
1105→1106[p_1|1]
1106→1070[p_1|1]
1107→1108[p_1|1]
1108→1109[p_1|1]
1109→1110[s_1|1]
1109→1112[f_1|2]
1110→1111[p_1|1]
1111→1112[f_1|1]
1112→1113[s_1|1]
1112→1115[s_1|2]
1113→1114[p_1|1]
1114→1115[s_1|1]
1115→1116[s_1|1]
1116→1071[p_1|1]
1117→1118[s_1|1]
1117→1120[p_1|2]
1118→1119[p_1|1]
1119→1120[p_1|1]
1120→1121[half_1|1]
1121→1072[s_1|1]
1121→1081[s_1|1]
1121→1121[s_1|1]
1122→1123[p_1|2]
1123→1124[p_1|2]
1124→1125[s_1|2]
1124→1127[f_1|3]
1125→1126[p_1|2]
1126→1127[f_1|2]
1127→1128[s_1|2]
1127→1130[s_1|3]
1128→1129[p_1|2]
1129→1130[s_1|2]
1130→1131[s_1|2]
1130→1103[s_1|2]
1131→1102[p_1|2]
1132→1133[p_1|2]
1133→1134[s_1|2]
1133→1136[s_1|3]
1133→1142[s_1|3]
1133→1144[p_1|3, p_1|4]
1134→1135[p_1|2]
1135→1136[s_1|2]
1135→1142[s_1|3]
1135→1144[p_1|4]
1136→1137[j_1|2]
1137→1138[s_1|2]
1138→1139[s_1|2]
1138→1096[s_1|2]
1138→1113[s_1|3, s_1|2]
1138→1115[s_1|3, s_1|2]
1138→1128[s_1|2, s_1|3]
1138→1130[s_1|2, s_1|3]
1138→1148[s_1|2, s_1|3]
1138→1150[s_1|2, s_1|3, s_1|4]
1139→1140[s_1|2]
1139→1095[p_1|3]
1140→1141[p_1|2]
1141→1095[p_1|2]
1142→1143[p_1|3]
1143→1144[p_1|3]
1144→1145[s_1|3]
1144→1147[f_1|4]
1145→1146[p_1|3]
1146→1147[f_1|3]
1147→1148[s_1|3]
1147→1150[s_1|4]
1148→1149[p_1|3]
1149→1150[s_1|3]
1150→1151[s_1|3]
1150→1138[s_1|3]
1151→1137[p_1|3]